#include "refactor.h"

inline unsigned varsig(unsigned i ){return 1<<(i+i) ; }
//=============================================================================
//  STATIC LOCAL FUNCTION
//=============================================================================
static unsigned use_lit( const cube_t f )
{
   unsigned n = 0;
   for( unsigned i = 0 ; i < f.size ; ++i )
      n |= f[i];
   return n;
}
static unsigned common_cube( const cube_t f )
{
   unsigned c = f[0];
   for( unsigned i = 1 ; i < f.size ; ++ i )
      c &= f[i];
   return c;
}
static unsigned make_cube_free( cube_t f )
{
   unsigned c = common_cube( f );
   if( c == 0 )return 0;
   for( unsigned i = 0 ; i < f.size ; ++ i )
      f[i] ^= c;
   return c;
}
static int less_lit_sig( unsigned sig , const cube_t f )
{
   unsigned short min_cnt=0xFFFF;
   unsigned short cnt ;
   unsigned min_lit;

   for( unsigned i = 1 ; i <= sig ; i += i )
   {
      cnt = 0;
      if( (i&sig) ==  0) continue;
      for( unsigned j = 0 ; j < f.size ; ++j )
         if(f[j]&i)cnt+=1; 
      if( cnt < 2 ) continue;
      if( cnt < min_cnt ){min_lit=i;min_cnt=cnt;if(min_cnt==2)break;}
   }
   if( min_cnt == 0xFFFF ) return -1;
   return min_lit;
}
static int less_lit_len( unsigned s , const cube_t f )
{
   unsigned short min_cnt=0xFFFF; 
   unsigned short cnt;
   unsigned min_lit;
   for( unsigned i = 1 ; i != s ; i+=i )
   {
      cnt = 0 ;
      for(unsigned j=0;j<f.size;++j) 
         if(f[j]&i)cnt+=1; 
      if(cnt<2)continue;
      if(cnt<min_cnt){min_lit=i,min_cnt=cnt;if(min_cnt==2)break;}
   }
   if(min_cnt==0xFFFF)return -1;
   return min_lit;
}
static int most_lit_sig( unsigned sig , const cube_t f  )
{
   unsigned short max_cnt=0;
   unsigned short cnt ;
   unsigned max_lit;

   for( unsigned i = 1 ; i <= sig ; i += i )
   {
      cnt = 0;
      if( (i&sig) ==  0) continue;
      for( unsigned j = 0 ; j < f.size ; ++j )
         if(f[j]&i)cnt+=1; 
      if( cnt > max_cnt ){max_lit=i;max_cnt=cnt;}
   }
   return max_lit;
}
static void divide( cube_t & f , unsigned d )
{
   unsigned k = 0 ;
   for( unsigned i = 0 ; i < f.size ; ++i )
      if( ((~f[i])&d) == 0 ) f[k++] = (f[i]^d);
   f.size = k;
}
//=============================================================================
//  DIVIDE
//=============================================================================
cube_t Refactor::divide( cube_t f , unsigned d )
{
   unsigned k = 0;
   for( unsigned i = 0 ; i < f.size ; ++ i ) 
      if( ((~f[i]) & d ) == 0 ) _mem[k++]=(f[i]^d);
   return allocate_cube( k );
}
cube_t Refactor::divide_rem( cube_t & f , unsigned d )
{
   unsigned k = 0;
   unsigned j = 0;
   for( unsigned i = 0 ; i < f.size ; ++i )
      if( ((~f[i]) & d ) == 0 ) _mem[k++]=(f[i]^d);
      else f[j++] = f[i];
   f.size = j;

   return allocate_cube( k );
}
cube_t Refactor::divide( cube_t f , cube_t q )
{
   unsigned k = 0 ; 
   for( unsigned i = 0 ; i < f.size ; ++ i )
   {
      if( ((~f[i]) & q[0]) == 0 )// f[i] contain q[0]
      {
         unsigned c = f[i] ^ q[0];

         bool isQ = true;
         for( unsigned j = 1 ; j < q.size ; ++ j )
         {
            bool contain = false;
            for( unsigned k = 0 ; k < f.size ; ++ k )
            {
               if( f[k] == (c | q[j]) )
               {
                  contain = true;
                  break;
               }
            }
            if( contain == false ){ isQ = false; break; }
         }
         if( isQ ) _mem[ k ++ ]= c ;
      }
   }
   return allocate_cube( k );
}
cube_t Refactor::divide( cube_t f , cube_t q , cube_t & d )
{
   static const unsigned dirty_bit = 0x80000000;
   static const unsigned clean_bits= 0x7FFFFFFF;
   d = allocate_cube( f.size/q.size ); d.size = 0;

   unsigned k = 0 , k2 = 0; 
   for( unsigned i = 0 ; i < f.size ; ++ i )
   {
      if( ((~f[i]) & q[0]) == 0 )// f[i] contain q[0]
      {
         unsigned c = f[i] ^ q[0];
         _mem[ k ++ ] = f[i];
         f[i] |= dirty_bit;

         bool isQ = true;
         for( unsigned j = 1 ; j < q.size ; ++ j )
         {
            bool contain = false;
            for( unsigned x = 0 ; x < f.size ; ++ x )
            {
               if( f[x] == (c | q[j]) )
               {
                  _mem[ k++ ] = f[x];
                  f[x] |= dirty_bit;
                  contain = true;
                  break;
               }
            }
            if( contain == false ){ isQ = false; break; }
         }
         if( isQ ){ k = k2 ; d[ d.size ++ ]= c ;}
         else k2 = k;
      }
   }
   for( unsigned i = 0 ; i < f.size ; ++ i )
      if( f[i] & dirty_bit ) f[i] &= clean_bits;
      else _mem[ k ++ ] = f[i];

   return allocate_cube( k );
}
//=============================================================================
//  CONSTRUCT 
//=============================================================================
AigLit Refactor::construct( cube_t f )
{
   if( f.size == 0 ) return toAigLit(0,0);
   AigLit p = construct( f[0] );
   for( unsigned i = 1 ; i < f.size ; ++i )
   {
      p = inv(createAND( inv(p) , inv(construct(f[i])) ));
   }
   return p;
}
AigLit Refactor::construct( unsigned c )
{
   if( c == 0 ) return toAigLit( 0 , 1 );
   AigLit q[12];
   unsigned k = 0;
   
   for( unsigned i = 1 , j = 0 ; i <= c ; i+=i , j +=1 ) 
      if( i & c )
      {
         q[ k ] = toAigLit( _cut[j/2] , j&1 );
         k+=1;
      }
   return build_blAND( q , k );
}
inline AigLit Refactor::ab_c( AigLit a , AigLit b , AigLit c )
{
   AigLit p = createAND(a,b);
   p = inv( createAND( inv(p) , inv(c) )); // OR
   return p;
}
//=============================================================================
//   QUICK DIVIDE CORE 
//=============================================================================

cube_t Refactor::quick_divisor( cube_t f )
{
   // terminal condition
   //if( f.size <= 1 ) return cube_t(0,0);

   // literal count
   int lit = less_lit_len( varsig(_cutSize), f );
   if( lit == -1 ) return cube_t(0,0);
   cube_t d = divide( f , lit );
   
   unsigned sig = use_lit( d );

   do
   {
      unsigned c = make_cube_free( d );
      sig ^= c;
      lit = less_lit_sig( sig , d );
      if( lit == -1 ) return d;
      ::divide( d , lit );
      sig ^= lit;
   }while(1);
}
AigLit Refactor::qfactor( cube_t f )
{
   if( f.size <= 1 ) return construct( f );
   
   unsigned * m = _mem;
   cube_t d = quick_divisor( f );
   if( d.empty() ) return construct( f );
   
   cube_t q = divide( f , d ); // divisor mutate
   if( q.size == 1 ) return lf( f , q[0] );
   
   make_cube_free( q );
   cube_t r = divide( f , q , d );
   unsigned c = common_cube( d );
   if( c == 0 )
   {
      m = _mem - r.size;
      AigLit rptr = r.size ? qfactor( r ) : 0; _mem = m;
      AigLit dptr = qfactor( d );              _mem = m -= d.size;
      AigLit qptr = qfactor( q );              
      return ab_c( qptr , dptr , rptr );
   }
   else
   {
      _mem = m;
      return lf( f , c );
   }

   return 0;
}
AigLit Refactor::lf( cube_t f , unsigned c )
{
   unsigned lit = most_lit_sig( c , f );
   cube_t q = divide_rem( f , lit );
   c = make_cube_free( q );

   unsigned * m = _mem;
   AigLit qptr = qfactor( q ); _mem = m - q.size ;
   AigLit rptr = qfactor( f ); 
   AigLit cptr = construct( lit|c );
   return ab_c( cptr , qptr , rptr );
}
